﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Epsilon.Expr;

namespace Epsilon.Typing
{
    public partial class TypeChecker
    {
        Process process;
        FunStore funStore;
        FunctionStore functionStore;
        SpecStore functionSpecs;
        public RxStore RxStore;

        public List<TxExpr> TxExprs { get; private set; }
        public List<SecConstraint> Constraints { get; private set; }

        public TypeChecker(Process p)
        {
            process = p;
            funStore = new FunStore();
            functionStore = new FunctionStore();
            functionSpecs = new SpecStore();
            RxStore = new RxStore();
            TxExprs = new List<TxExpr>();
            Constraints = new List<SecConstraint>();

            process.RxStore = this.RxStore;
        }

        public void Error(string message, Expression e)
        {
            string s = "Error - " + message;
            if (e != null)
                s += "\nprocess: " + process.Name + " line: " + e.Line + " col: " + e.Col;
            throw new TypingException(s);
        }

        public TypeLabel JoinMeet(Type t, List<TypeLabel> labels)
        {
            List<PidLabel> pplus = new List<PidLabel>();
            List<PidLabel> pminus = new List<PidLabel>();
            List<SecLabel> sec = new List<SecLabel>();

            for (int i = 0; i < labels.Count; i++)
            {
                pplus.Add(labels[i].MaxPidLabel);
                pminus.Add(labels[i].MinPidLabel);
                sec.Add(labels[i].SecLabel);
            }

            return new TypeLabel(
                t,
                PidUtil.Join(pplus),
                PidUtil.Meet(pminus),
                SecUtil.Meet(sec)
                );
        }

        public void TypeCheck()
        {
            // first add all the functions
            for (int i = 0; i < process.Functions.Count; i++)
                functionStore.AddFunction(process.Functions[i]);

            // and all the specs
            foreach (string k in process.Specs.Keys)
                functionSpecs.AddSpec(k, process.Specs[k]);

            // now type-check them all under a blank context
            Context c = new Context(process.Name, process.Records);

            bool changed = false;
            //int tries = 0;
            do
            {
                //tries++;
                changed = false;
                for (int i = 0; i < process.Functions.Count; i++)
                {
                    Tuple<FunType, PidFun, PidFun, SecFun> init =
                        functionStore.GetLabels(process.Functions[i].Name, process.Functions[i].ArgumentTypes);

                    TypeLabel newtl = TypeCheck(c, process.Functions[i]);

                    if (((PidFun)(newtl.MaxPidLabel)) != init.Item2 ||
                        ((PidFun)(newtl.MinPidLabel)) != init.Item3 ||
                        ((SecFun)(newtl.SecLabel)) != init.Item4)
                    {
                        changed = true;
                        functionStore.UpdateLabels(process.Functions[i].Name, process.Functions[i].ArgumentTypes,
                            ((PidFun)(newtl.MaxPidLabel)).Ret,
                            ((PidFun)(newtl.MinPidLabel)).Ret,
                            ((SecFun)(newtl.SecLabel)).Ret);
                    }
                }
                //} while (changed && (tries < 10));
            } while (changed);
        }

        public void AddConstraint(SecConstraint c)
        {
            foreach (SecConstraint sc in Constraints)
            {
                if (sc.Label.SecV != c.Label.SecV)
                    continue;

                if ((sc.Process is PidExpr) && (c.Process is PidExpr) &&
                    ((PidExpr)sc.Process).Pid == ((PidExpr)c.Process).Pid)
                    return;

                if ((sc.Process is PidVar) && (c.Process is PidVar) &&
                    ((PidVar)sc.Process).PidV == ((PidVar)c.Process).PidV)
                    return;
            }

            // Now find out which clause contains the variables
            List<RxClauseExpr> clauses = RxStore.GetAllClauses();

            foreach (RxClauseExpr clause in clauses)
            {
                SecRLabel sec = RxStore.GetRxSecArg(clause);
                PidRLabel pid = RxStore.GetRxPidMaxArg(clause);
                bool hasSec = false, hasPid = false;

                if (SecUtil.Vars(sec).Contains(c.Label))
                    hasSec = true;

                if (c.Process is PidVar)
                {
                    if (PidUtil.Vars(pid).Contains((PidVar)c.Process))
                        hasPid = true;
                }
                else
                    hasPid = true;

                if (hasSec && !hasPid)
                    Error("Unable to satisfy a constraint where the pid and sec " +
                        "variables are from different rx clauses", null);

                if (hasSec && hasPid)
                {
                    c.Clause = clause;
                    break;
                }
            }

            Constraints.Add(c);
        }
    }

    public class SecConstraint
    {
        public ISecPid Process { get; private set; }
        public SecVar Label { get; private set; }
        public RxClauseExpr Clause { get; set; }

        public SecConstraint(ISecPid proc, SecVar lab)
        {
            Process = proc;
            Label = lab;
            Clause = null;
        }
    }
}
